278 X EXISTENCE THEOREMS

We write the proof for continuously differentiable mappings, the modifica-
tions in the other cases being obvious.

We may suppose 0 = 0, & = 0, replacing /by the mapping x -*f(a -f x) — i.
Let M be the kernel of the linear mapping /'(O), which is an (n -p)-dimen-
sional subspace of E, and let N be a (p-dimensional) supplement of M in E ; we
take as a basis of E a system (c^i^n ofn vectors such that c1? . . ,, cp forma

n

basis of N, cp+l9 . . . , cn a basis of M, and we write x = ^ <P&)cs for any

»=i
x e E, the (pt being linear forms. Ifel9...9enis the canonical basis of K\ we

n

denote by x~*G(x) the linear mapping x-+ ]T <piO)^ of E onto the

i-p+l

subspace Kn~p of K" generated by the el of index z > /?.

Let P be the image of E (and of N) by the linear mapping /'(O); it is a
p-dimensional subspace of F, having the elements dt =/'(0) • ct (1 ^ / ^p)
as a basis; we take a basis (dj)^^ of F, of which the preceding basis

of P form the first p elements, and we write y = ]£ ^j(y)dj for anyy e F, the

j = i
i/^. being linear forms. We denote by y-*H(y) the linear mapping

p
y "-* Z ^j(y)ej °f F onto ^e subspace Kp of K" generated by the e,. of index

We now consider the mapping x -+ ^(x) = H(f(xJ) 4- <?O) of A into K"
which is continuously differentiable. Moreover, by (8.1.3) and (8.2.1), ^we
have g'(x) • s = H(f'(x) - s) + G(s) for any s e E, hence ^'(0) - c{ == et for
1 < f < n (i.e. ^'(°) is represented by the unit matrix with respect to tie bases
(cj) and (e^). Using (10.2.5), we conclude that there is an open neighborhood
U0 c A of 0 such that the restriction of g to U0 is a homeomorphism of TJ0
onto an open neighborhood of 0 in Kw, and that the inverse homeomorphism
g~l is continuously differentiable in #(U0). Let r > 0 be such that the ball
|x£| < r (1 < / < n) is contained in ^(U0), and let U be the inverse image of
that ball by g, which is an open neighborhood of 0; our mapping t/r will be

the restriction to U of the mapping x -> - g(x).

Up to now we have not used the assumption that the rank of f'(x) is
constant in A; this implies that the image Px of E by/'(*) has dimension p
for any x e A. Now we may suppose U0 has been taken small enough so
that g'(x) is a linear bijection of E onto K" for x e U0 (8.3.2); as Pve have
g'(x) • s = H(f'(x) - s) for s e N, the restriction of f'(x) to N must be a
bijection of that ^-dimensional space onto fx , and the restriction of H to
Px a bijection of Px onto Kp. Denote by Lx the bijection of Kp onto fx , inverse
of the preceding mapping; we can thus write /'(*) = Lx ° H9.17.3) to x — sf(x, y), considered as a function of x; this defines an analytic function